Termination w.r.t. Q proof of /tmp/tmpvT3EjD/matchbox2.srs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

N(s(x1)) → T(x1)
T(e(x1)) → N(s(x1))
T(e(x1)) → S(x1)
A(l(x1)) → A(t(x1))
S(a(x1)) → A(t(e(x1)))
S(a(x1)) → O(m(a(t(e(x1)))))
A(l(x1)) → T(x1)
N(s(x1)) → A(l(a(t(x1))))
O(m(a(x1))) → T(e(n(x1)))
S(a(x1)) → T(o(m(a(t(e(x1))))))
T(o(x1)) → A(x1)
S(a(x1)) → T(e(x1))
N(s(x1)) → A(t(x1))
S(a(x1)) → A(t(o(m(a(t(e(x1)))))))
O(m(a(x1))) → N(x1)

The TRS R consists of the following rules:

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

N(s(x1)) → T(x1)
T(e(x1)) → N(s(x1))
T(e(x1)) → S(x1)
A(l(x1)) → A(t(x1))
S(a(x1)) → A(t(e(x1)))
S(a(x1)) → O(m(a(t(e(x1)))))
A(l(x1)) → T(x1)
N(s(x1)) → A(l(a(t(x1))))
O(m(a(x1))) → T(e(n(x1)))
S(a(x1)) → T(o(m(a(t(e(x1))))))
T(o(x1)) → A(x1)
S(a(x1)) → T(e(x1))
N(s(x1)) → A(t(x1))
S(a(x1)) → A(t(o(m(a(t(e(x1)))))))
O(m(a(x1))) → N(x1)

The TRS R consists of the following rules:

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

N(s(x1)) → T(x1)
T(e(x1)) → N(s(x1))
T(e(x1)) → S(x1)
S(a(x1)) → A(t(e(x1)))
S(a(x1)) → O(m(a(t(e(x1)))))
A(l(x1)) → T(x1)
N(s(x1)) → A(l(a(t(x1))))
O(m(a(x1))) → T(e(n(x1)))
S(a(x1)) → T(o(m(a(t(e(x1))))))
T(o(x1)) → A(x1)
S(a(x1)) → T(e(x1))
N(s(x1)) → A(t(x1))
O(m(a(x1))) → N(x1)

The remaining pairs can at least be oriented weakly.

A(l(x1)) → A(t(x1))
S(a(x1)) → A(t(o(m(a(t(e(x1)))))))

Used ordering: Polynomial interpretation [25,35]:

POL(l(x₁)) = (1/4)x_1
POL(m(x₁)) = (1/4)x_1
POL(O(x₁)) = 4 + x_1
POL(N(x₁)) = 1/4 + (1/2)x_1
POL(T(x₁)) = x_1
POL(n(x₁)) = (1/4)x_1
POL(t(x₁)) = (1/4)x_1
POL(a(x₁)) = 1/2 + (4)x_1
POL(e(x₁)) = 4 + (4)x_1
POL(A(x₁)) = 1/4 + (4)x_1
POL(s(x₁)) = 4 + (4)x_1
POL(o(x₁)) = 1 + (4)x_1
POL(S(x₁)) = 15/4 + (4)x_1

The value of delta used in the strict ordering is 1/8.
The following usable rules [17] were oriented:

t(e(x1)) → n(s(x1))
t(o(x1)) → m(a(x1))
o(m(a(x1))) → t(e(n(x1)))
a(l(x1)) → a(t(x1))
n(s(x1)) → a(l(a(t(x1))))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

A(l(x1)) → A(t(x1))
S(a(x1)) → A(t(o(m(a(t(e(x1)))))))

The TRS R consists of the following rules:

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

A(l(x1)) → A(t(x1))

The TRS R consists of the following rules:

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

A(l(x1)) → A(t(x1))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(n(x₁)) = 3
POL(l(x₁)) = 4
POL(m(x₁)) = 0
POL(t(x₁)) = 3
POL(a(x₁)) = 3
POL(A(x₁)) = (4)x_1
POL(e(x₁)) = 4
POL(s(x₁)) = 5/4 + (3)x_1
POL(o(x₁)) = 3 + (3)x_1

The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented:

t(e(x1)) → n(s(x1))
t(o(x1)) → m(a(x1))
o(m(a(x1))) → t(e(n(x1)))
a(l(x1)) → a(t(x1))
n(s(x1)) → a(l(a(t(x1))))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.